r:. 0 < -(r)  r < 0 

latex

Definitions	P  Q, P  Q, True, T, P  Q, P & Q, , r - s, qpositive(r), t.1, r + s, q_le(r;s), qeq(r;s), t.2, , gset, , x f y, a < b, goset, a <p b, 1/r, ff, tt, if b then t else f fi , <+>, a < b, t  T, (r/s), A, r * s, r < s, P  Q, x:A. B(x), False, a  b  T , A c B, , x:A. B(x), S  T
Lemmas	not functionality wrt iff, assert of bnot, assert of eq int, assert of lt int, or functionality wrt iff, assert of bor, and functionality wrt iff, assert of band, iff transitivity, iff functionality wrt iff, true wf, squash wf, not wf, bnot wf, eq int wf, lt int wf, bor wf, band wf, assert wf, rationals wf, qmul wf, int inc rationals, qless wf, iff wf, int nzero properties, q-elim